Nuprl Lemma : f2f+-p+-total
11,40
postcript
pdf
es
:ES,
ff
:FIFO,
f2f+
:F2F+-decls.
plus-ify{i:l}(
es
;
ff
;is_req ;is_ack ;awaiting ;owes_ack )
(
sndr
,
rcvr
:
ff
.C,
e
,
e'
:E.
([
e
:
sndr
is_req
rcvr
]
[
e
:
rcvr
is_ack
sndr
])
([
e'
:
sndr
is_req
rcvr
]
[
e'
:
rcvr
is_ack
sndr
])
(((f2f+-p+(
e
,
e'
))
(
e
=
e'
))
(f2f+-p+(
e'
,
e
))))
latex
Definitions
x
(
s
)
,
A
c
B
,
,
t
T
,
P
&
Q
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
f
y
,
{
T
}
,
f2f+-p+
Lemmas
f2f+-pred-field
,
f2f+-pred
wf
,
generated-thread-properties2
,
f2f+-pred-generates-thread
,
event
system
wf
,
FIFO
wf
,
F2F+-decls
wf
,
fifoS
wf
,
fifoR
wf
,
f2f+Owes
wf
,
f2f+Wait
wf
,
plus-ify
wf
,
fifoC
wf
,
es-E
wf
,
f2f+Ack
wf
,
f2f+Req
wf
,
snd-it
wf
,
f2f+-property
origin